module Zeno.FL 
(
  findAndParseFL
)
where

import Prelude ()
import StdImports
import qualified Data.Map as Map
import qualified Data.IntMap as IMap

import Zeno.Core
import Zeno.FLParser

-- TODO optimize: does a heavy function name lookup 
--   for every function name occurrence

type FL = StateT (Map String ZVar) ZenoState
          
findAndParseFL :: String -> ZenoState ()
findAndParseFL fl = do
  let lemmas = parseFL fl
  flip evalStateT Map.empty $
    mapM_ parseLemma lemmas

parseLemma :: Lemma -> FL ()
parseLemma (Lemma name vars eq conds) = do
  vars' <- mapM addVariable vars
  eq' <- mapPairM (mapM lookupVar) eq
  conds' <- mapM (mapPairM (mapM lookupVar)) conds
  lift $ addLemma name (Clause vars' eq' conds')
  
lookupVar :: String -> FL ZVar
lookupVar name = do
  vars <- get
  case Map.lookup name vars of
    Just zvar -> return zvar
    Nothing -> lift $ readonly $ getGlobalVar name

addVariable :: (String, Type String) -> FL ZVar
addVariable (name, str_type) = do
  var_type <- lift $ readonly $ mapM findDataType str_type
  var_id <- lift newIdS
  let var = ZVar var_id var_type ZVariable
  lift $ christen var_id name
  modify $ Map.insert name var
  return var
